#!/usr/bin/env python


class SAT:
    def __init__(self, clauses):
        """variable x_1 is denotet by '1', its negation by '-1'.
        clauses is a list of varible-lists:
        (x_1 or not x_2) and (x_2) == ((1, -2), (2,))."""
        self.num_variables = len(set(abs(x) for xs in clauses for x in xs))
        self.num_clauses = len(clauses)
        self.clauses = clauses

    def num_satisfied_clauses(self, variables):
        """variables is a list of True/False or 1/0 values."""
        counter = 0

        for clause in self.clauses:
            for literal in clause:
                if ((literal < 0 and variables[abs(literal) - 1] in (False, 0, 0.0)) or
                    (literal > 0 and variables[literal - 1] in (True, 1, 1.0))):
                    counter += 1
                    #print "counter increased"
                    break
            else:
                pass
                #print "did not count some item."
                #import pdb
                #pdb.set_trace()
        return counter

    def __repr__(self):
        return """<MaxSAT {0} variables, {1} clauses>""".format(
            self.num_variables, self.num_clauses)

    def generate_ip(self):
        import gurobipy as grb
        m = grb.Model(self.__repr__())

        # add variables
        literals = [m.addVar(vtype=grb.GRB.BINARY, name="x_{0}".format(i))
                        for i in xrange(1, self.num_variables + 1)]
        clauses = [m.addVar(vtype=grb.GRB.BINARY, obj=1,
                        name="clause_{0}".format(i)) for i in
                        xrange(1, self.num_clauses + 1)]
        m.update()

        # add constraints
        for clause, clause_indicator in zip(self.clauses, clauses):
            #print clause, clause_indicator
            pos_vars = grb.quicksum(literals[i - 1] for i in clause if i > 0)
            neg_vars = grb.quicksum(1 - literals[abs(i) - 1] for i in clause if i < 0)
            m.addConstr(pos_vars + neg_vars >= clause_indicator)
        m.update()

        # maximize clauses
        m.modelSense = -1
        return m

    @staticmethod
    def from_file(filename):
        with open(filename) as f:
            clauses = []
            current_clause = []
            for line in f:
                if line.startswith("c") or line.startswith("p"):
                    continue
                nums = map(int, line.split())
                for num in nums:
                    if num == 0:
                        clauses.append(current_clause)
                        current_clause = []
                    else:
                        current_clause.append(num)
        return SAT(clauses)


def satEA(instance):
    from pyevolve import G1DBinaryString, GSimpleGA
    #eval_func = lambda s: instance.num_satisfied_clauses(s)

    def eval_func(s, instance=instance):
        return instance.num_satisfied_clauses(s.genomeList)

    #eval_func = partial(eval_func, instance=instance)

    # Genome instance
    genome = G1DBinaryString.G1DBinaryString(instance.num_variables)

    # The evaluator function (objective function)
    genome.evaluator.set(eval_func)
    ga = GSimpleGA.GSimpleGA(genome)

    # some paramters
    ga.setGenerations(1000)
    #ga.setCrossoverRate(1.0)
    ga.setMutationRate(0.1)
    ga.setPopulationSize(100)

    # Do the evolution, with stats dump
    # frequency of 10 generations
    ga.setInteractiveGeneration(1)
    ga.evolve(freq_stats=10)

    # Best individual
    print ga.bestIndividual()
